﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using System.Diagnostics.Contracts;

using SimpleIR;
using PInfoModel;

namespace TestGen
{
	public class ModelSizeInfo
	{
		private PIModel m_pim;
		private List<TGenConstraint> m_genconstraints;
		private Dictionary<int, string> m_idToContainerCardNameMap;
		private Dictionary<int, string> m_idToRgnCardMap;
		private Dictionary<PointerSetInfoTuple, string> m_idToPtrSetCardMap;

		private ModelSizeInfo(PIModel pim)
		{
			this.m_pim = pim;
			this.m_genconstraints = new List<TGenConstraint>();
			this.m_idToContainerCardNameMap = new Dictionary<int, string>();
			this.m_idToRgnCardMap = new Dictionary<int, string>();
			this.m_idToPtrSetCardMap = new Dictionary<PointerSetInfoTuple, string>();
		}

		public static void ComputeConstraintSets(PIModel m, List<TGenConstraint> constraints, List<Tuple<string, string>> fixedvars, List<string> paramargs)
		{
			ModelSizeInfo msi = new ModelSizeInfo(m);
			msi.ComputeRegionSizeParamsAndBasicConstraints();
			msi.ComputePtrEdgeSizeParams();
			msi.ComputeEdgeSizeContraints_OutEdges();
			msi.ComputeEdgeSizeContraints_InEdges();

			ConstraintSolve.GenerateSimplifiedConstraints(msi.m_genconstraints, constraints, fixedvars);

			paramargs.AddRange(msi.m_idToContainerCardNameMap.Values);
			paramargs.AddRange(msi.m_idToRgnCardMap.Values);
			paramargs.AddRange(msi.m_idToPtrSetCardMap.Values);

			paramargs.RemoveAll((string vn) => fixedvars.Exists((Tuple<string, string> fpv) => vn.Equals(fpv.Item1)));
		}

		/// <summary>
		/// For each region genrate the needed names for the size variables and assert the basic constraints on their sizes.
		/// </summary>
		private void ComputeRegionSizeParamsAndBasicConstraints()
		{
			foreach(PIMNode hr in this.m_pim.Nodes)
			{
				if(hr.LocationType is IRContainerType)
				{
					string cardParam = NameGen.GenerateNameForRegionCardinality(hr);
					this.m_idToContainerCardNameMap.Add(hr.LocationAddress, cardParam);
					TGenVar vterm = new TGenVar(cardParam);

					if(hr.ContainerMustBeEmpty)
					{
						TGenConst cval = new TGenConst(0);
						TGenConstraint cst = new TGenConstraint(ConstraintType.Equality, vterm, cval);
						this.m_genconstraints.Add(cst);
					}
					else
					{
						TGenConst cval = new TGenConst(0);
						TGenConstraint cst = new TGenConstraint(ConstraintType.GreaterEqual, vterm, cval);
						this.m_genconstraints.Add(cst);
					}
				}
			}

			foreach(PIMNode hr in this.m_pim.Nodes)
			{
				string rgntypename = NameGen.GenerateNameForRegionCount(hr);
				this.m_idToRgnCardMap.Add(hr.LocationAddress, rgntypename);

				if(hr.HomeLocFor != null)
					this.m_genconstraints.Add(new TGenConstraint(ConstraintType.Equality, new TGenVar(rgntypename), new TGenConst(1)));
				else
				{
					//always |RgnT| >= 0
					this.m_genconstraints.Add(new TGenConstraint(ConstraintType.GreaterEqual, new TGenVar(rgntypename), new TGenConst(0)));

					//|Rgn| <= 1 if possible
					if(hr.IsUniqueLocation)
						this.m_genconstraints.Add(new TGenConstraint(ConstraintType.LessEqual, new TGenVar(rgntypename), new TGenConst(1)));
				}
			}
		}

		/// <summary>
		/// For each ptr edge generate the needed names for the size variables and assert the basic constraints on their sizes.
		/// </summary>
		private void ComputePtrEdgeSizeParams()
		{
			foreach(PIMNode hrs in this.m_pim.Nodes)
			{
				if(hrs.HomeLocFor != null)
				{
					foreach(PIMEdge ee in hrs.OutEdges)
					{
						string vename = NameGen.GenerateNameForPtrSetCount(ee.SourceAddress, ee.TargetAddress, "H");
						PointerSetInfoTuple pstup = new PointerSetInfoTuple(ee.SourceAddress, ee.TargetAddress, "H");
						this.m_idToPtrSetCardMap.Add(pstup, vename);

						//if unique and non-null then |E| == 1 else |E| <= 1
						if(ee.IsNonNull && hrs.OutEdges.Count == 1)
							this.m_genconstraints.Add(new TGenConstraint(ConstraintType.Equality, new TGenVar(vename), new TGenConst(1)));
						else
						{
							//always 0 <= |E| <= 1
							this.m_genconstraints.Add(new TGenConstraint(ConstraintType.GreaterEqual, new TGenVar(vename), new TGenConst(0)));
							this.m_genconstraints.Add(new TGenConstraint(ConstraintType.LessEqual, new TGenVar(vename), new TGenConst(1)));
						}
					}
				}
				else
				{
					foreach(PIMEdge ee in hrs.OutEdges)
					{
						string vename = NameGen.GenerateNameForPtrSetCount(ee.SourceAddress, ee.TargetAddress, ee.OffsetInSource.PathFirst.FieldName);
						PointerSetInfoTuple pstup = new PointerSetInfoTuple(ee.SourceAddress, ee.TargetAddress, ee.OffsetInSource.PathFirst.FieldName);
						this.m_idToPtrSetCardMap.Add(pstup, vename);

						string snname = this.m_idToRgnCardMap[hrs.LocationAddress];

						if(ee.IsNonNull && hrs.OutEdges.Count == 1 && (hrs.IsUniqueLocation || !ee.OffsetInSource.AccessPathHasSummaryLocation))
							new TGenConstraint(ConstraintType.Equality, new TGenVar(vename), new TGenVar(snname));
						else
						{
							string cname = this.m_idToContainerCardNameMap[hrs.LocationAddress];
							TGenTerm snsizet = new TGenBinMult(new TGenVar(snname), new TGenVar(cname));

							//always 0 <= |E| <= snsizet
							this.m_genconstraints.Add(new TGenConstraint(ConstraintType.GreaterEqual, new TGenVar(vename), new TGenConst(0)));
							this.m_genconstraints.Add(new TGenConstraint(ConstraintType.LessEqual, new TGenVar(vename), snsizet));
						}
					}
				}
			}
		}

		/// <summary>
		/// For each node compute the constraints between the region sizes and the OUT edges.
		/// </summary>
		private void ComputeEdgeSizeContraints_OutEdges()
		{
			foreach(PIMNode hr in this.m_pim.Nodes)
			{
				foreach(IRBasicAccessPath bap in hr.LocationType.TypeDescription.AllTerminalAccessPaths)
				{
					PIMEdge[] esl = hr.OutEdges.Where((PIMEdge ee) => ee.OffsetInSource == bap).ToArray();
					if(esl.Length == 0)
						continue;

					TGenTerm sourcesum;
					if(!bap.AccessPathHasSummaryLocation)
						sourcesum = new TGenVar(this.m_idToRgnCardMap[hr.LocationAddress]);
					else
						sourcesum = new TGenBinMult(new TGenVar(this.m_idToRgnCardMap[hr.LocationAddress]), new TGenVar(this.m_idToContainerCardNameMap[hr.LocationAddress]));

					TGenTerm[] edgesumarr = new TGenTerm[esl.Length];
					for(int i = 0; i < esl.Length; ++i)
					{
						PIMEdge te = esl[i];
						PointerSetInfoTuple pst = new PointerSetInfoTuple(te.SourceAddress, te.TargetAddress, (hr.HomeLocFor != null) ? "H" : te.OffsetInSource.PathFirst.FieldName);
						edgesumarr[i] = new TGenVar(this.m_idToPtrSetCardMap[pst]);
					}
					TGenSum edgesum = new TGenSum(edgesumarr);

					bool isnonnull = esl.Any((PIMEdge ee) => ee.IsNonNull);
					bool notcontaineroronly1 = hr.IsUniqueLocation || !bap.AccessPathHasSummaryLocation;

					if(isnonnull & notcontaineroronly1)
						this.m_genconstraints.Add(new TGenConstraint(ConstraintType.Equality, edgesum, sourcesum));
					else
						this.m_genconstraints.Add(new TGenConstraint(ConstraintType.LessEqual, edgesum, sourcesum));
				}
			}
		}

		/// <summary>
		/// For each node compute the constraints between the region sizes and the IN edges.
		/// </summary>
		private void ComputeEdgeSizeContraints_InEdges()
		{
			foreach(PIMNode hr in this.m_pim.Nodes)
			{
				if(hr.HomeLocFor != null)
					continue;

				if(hr.InEdges.Count == 1)
				{
					PIMEdge sie = hr.InEdges[0];
					PointerSetInfoTuple pst = new PointerSetInfoTuple(sie.SourceAddress, sie.TargetAddress, (sie.OffsetInSource == IRBasicAccessPath.EmptyAccessPath ? "H" : sie.OffsetInSource.PathFirst.FieldName));
					TGenVar edgeterm = new TGenVar(this.m_idToPtrSetCardMap[pst]);

					TGenVar hrt = new TGenVar(this.m_idToRgnCardMap[hr.LocationAddress]);
					
					if(sie.IsInjective)
						this.m_genconstraints.Add(new TGenConstraint(ConstraintType.Equality, edgeterm, hrt));
					else
						this.m_genconstraints.Add(new TGenConstraint(ConstraintType.GreaterEqual, edgeterm, hrt));
				}
				else
				{
					TGenTerm[] edgesumarr = new TGenTerm[hr.InEdges.Count];
					for(int i = 0; i < hr.InEdges.Count; ++i)
					{
						PIMEdge sie = hr.InEdges[0];
						PointerSetInfoTuple pst = new PointerSetInfoTuple(sie.SourceAddress, sie.TargetAddress, (sie.OffsetInSource == IRBasicAccessPath.EmptyAccessPath ? "H" : sie.OffsetInSource.PathFirst.FieldName));
						edgesumarr[i] = new TGenVar(this.m_idToPtrSetCardMap[pst]);
					}
					TGenSum edgesum = new TGenSum(edgesumarr);

					TGenVar hrt = new TGenVar(this.m_idToRgnCardMap[hr.LocationAddress]);

					this.m_genconstraints.Add(new TGenConstraint(ConstraintType.GreaterEqual, edgesum, hrt));
				}
			}
		}
	}

	public struct PointerSetInfoTuple : IEquatable<PointerSetInfoTuple>
	{
		public readonly int Source;
		public readonly int Target;
		public readonly string OnField;

		public PointerSetInfoTuple(int source, int target, string f)
		{
			this.Source = source;
			this.Target = target;
			this.OnField = f;
		}

		public override string ToString()
		{ return "(" + this.Source + "." + this.OnField + " ->" + this.Target + ")"; }

		public override int GetHashCode()
		{ return this.Source ^ this.Target ^ this.OnField.GetHashCode(); }

		public override bool Equals(object obj)
		{ return (obj is PointerSetInfoTuple) && this.Equals((PointerSetInfoTuple)obj); }

		public bool Equals(PointerSetInfoTuple other)
		{ return (this.Source == other.Source) & (this.Target == other.Target) & this.OnField.Equals(other.OnField); }
	}

	/// <summary>
	/// A simple struct for representing how to select node/edge paramemters, they can be variables that pex instantiates or constants.
	/// </summary>
	public struct SelectionParameter
	{
		private readonly int m_selectionConst;
		private readonly string m_selectionParam;

		public SelectionParameter(int iv)
		{
			Contract.Requires(iv >= 0);

			this.m_selectionConst = iv;
			this.m_selectionParam = null;
		}

		public SelectionParameter(string sv)
		{
			Contract.Requires(sv != null);

			this.m_selectionConst = Int32.MinValue;
			this.m_selectionParam = sv;
		}

		public override string ToString()
		{
			return this.CodeValString;
		}

		public string CodeValString
		{
			get
			{
				return this.IsParamVal ? this.ParamVal : this.ConstVal.ToString();
			}
		}

		public bool IsConstVal { get { return this.m_selectionConst != Int32.MinValue; } }

		public int ConstVal
		{
			get
			{
				Contract.Requires(this.IsConstVal);
				return this.m_selectionConst;
			}
		}

		public bool IsParamVal { get { return this.m_selectionParam != null; } }

		public string ParamVal
		{
			get
			{
				Contract.Requires(this.IsParamVal);
				return this.m_selectionParam;
			}
		}
	}
}
